| Definitions | (x  l), x dom(f), True, False, inl x , tt, inr x , ff, loc(e), {x:A| B(x)} , as @ bs, es-interface-history(es; X; e), E(X), filter(P;l), X(e), [], e  X, if b then t else f fi , case b of inl(x) => s(x) | inr(y) => t(y), (e < e'), t.1, (e <loc e'), {T}, x(s), let x,y = A in B(x;y), wellfounded{i:l}(A; x,y.R(x;y)), AbsInterface(A), E, P & Q,   x. t(x), x.A(x), pred(e), <a, b>,  A, first(e), suptype(S; T), S  T, Top,  x:A.B(x), !Void(), x,y. t(x;y), pred!(e;e'),  , SWellFounded(R(x;y)), constant_function(f;A;B),  b,  , e < e', r  s, val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time),  , type List, Msg(M), kind(e), loc(e), Knd, kindcase(k; a.f(a); l,t.g(l;t) ), EOrderAxioms(E; pred?; info), x:A  B(x), IdLnk, left + right, Unit, EqDecider(T), Type, P   Q, strong-subtype(A;B),  , Id, f(a), a:A fp B(a), EState(T), ES,  x:A. B(x), x:A B(x), t T, s = t, P  Q, s ~ t, SQType(T), p q, p  q, p q, e = e', deq-member(eq;x;L), a = b, a = b, qeq(r;s), q_less(a;b), q_le(r;s), eq_atom$n(x;y), [d], a < b, x f y, a < b, null(as), x =a y, (i = j), i z j, i <z j, p =b q, b, prior(X), f(x)?z, P  Q, P Q,  x:A. B(x), A c B, e loc e' ,  T, ma-state(ds), decl-state(ds), es-state(es; i), es-vartype(es; i; x), f g, es-init(es;e), lastchange(x;e), e c e', pred(e), (last change to x before e), @e(x v), e(e1,e2].P(e), IsPrimeIdeal(R;P), IsIntegDom(r), a b, IsMonHom{M1,M2}(f), IsGroup(T;op;id;inv), IsMonoid(T;op;id), monot(T;x,y.R(x;y);f), Cancel(T;S;op), FunThru2op(A;B;opa;opb;f), fun_thru_1op(A;B;opa;opb;f), Dist1op2opLR(A;1op;2op), IsAction(A;x;e;S;f), IsBilinear(A;B;C;+a;+b;+c;f), BiLinear(T;pl;tm), Inverse(T;op;id;inv), Comm(T;op), Assoc(T;op), Ident(T;op;id), CoPrime(a,b), Connex(T;x,y.R(x;y)), AntiSym(T;x,y.R(x;y)), Trans(T;x,y.E(x;y)), Sym(T;x,y.E(x;y)), Refl(T;x,y.E(x;y)), IsEqFun(T;eq), Inj(A;B;f), InvFuns(A;B;f;g), a =!x:T. Q(x), SqStable(P), e(e1,e2].P(e), e[e1,e2].P(e), e[e1,e2].P(e), e[e1,e2).P(e), e[e1,e2).P(e), ee'.P(e), e<e'. P(e), ee'.P(e), e<e'.P(e), l_disjoint(T;l1;l2), Outcome, q-rel(r;x), r < s, (xL.P(x)), xL. P(x), a < b, a <p b, a b, a ~ b, b | a, Dec(P), locl(a), rcv(l; tg) |
| Lemmas | subtype rel list, subtype rel function, append-nil, es-le weakening, es-locl transitivity2, es-causl weakening, decidable assert, sq stable from decidable, es-prior-interface-locl, es-le-prior-interface-val, es-causle-le, es-E-interface-subtype rel, squash wf, filter append sq, es-interface-subtype rel, es-is-prior-interface, bnot wf, es-prior-interface wf, assert of bnot, eqff to assert, iff transitivity, bool sq, guard wf, eqtt to assert, bool cases, es-interface-history-prior, event system wf, subtype rel wf, EState wf, Id wf, rationals wf, member wf, strongwellfounded wf, pred! wf, unit wf, top wf, first wf, assert wf, not wf, loc wf, constant function wf, IdLnk wf, kindcase wf, Knd wf, bool wf, qle wf, cless wf, val-axiom wf, nat wf, Msg wf, kind wf, EOrderAxioms wf, deq wf, es-E wf, es-interface-val wf, append wf, es-E-interface wf, es-interface-val wf2, filter wf, es-locl wf, es-causl wf, es-loc wf, es-is-interface wf, es-interface wf, bfalse wf, btrue wf, false wf, true wf, es-interface-history wf, es-locl-wellfnd |
